the_es:ES, j:E, m:Msg. (isrcv(j))  (haslink(lnk(j);m)  Type) 

latex

Definitions	x:A. B(x), P  Q, t  T, haslink(l;m),
Lemmas	IdLnk wf, mlnk wf2, es-lnk wf, assert wf, es-isrcv wf, es-Msg wf, es-E wf, event system wf